Termination w.r.t. Q proof of /tmp/tmp5Ik3W8/otto13.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
LE(0, y, z) → GREATER(y, z)
GREATER(s(x), s(y)) → GREATER(x, y)
TRIPLE(x) → DOUBLE(x)
TRIPLE(x) → LE(x, x, double(x))
LE(s(x), s(y), s(z)) → LE(x, y, z)
DOUBLE(s(x)) → DOUBLE(x)
IF(first, x, y, z) → LE(s(x), y, s(z))
IF(second, x, y, z) → LE(s(x), s(y), z)
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
TRIPLE(x) → IF(le(x, x, double(x)), x, 0, 0)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
LE(0, y, z) → GREATER(y, z)
GREATER(s(x), s(y)) → GREATER(x, y)
TRIPLE(x) → DOUBLE(x)
TRIPLE(x) → LE(x, x, double(x))
LE(s(x), s(y), s(z)) → LE(x, y, z)
DOUBLE(s(x)) → DOUBLE(x)
IF(first, x, y, z) → LE(s(x), y, s(z))
IF(second, x, y, z) → LE(s(x), s(y), z)
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
TRIPLE(x) → IF(le(x, x, double(x)), x, 0, 0)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 6 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DOUBLE(s(x)) → DOUBLE(x)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

DOUBLE(s(x)) → DOUBLE(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(DOUBLE(x₁)) = (2)x_1
POL(s(x₁)) = 4 + (4)x_1

The value of delta used in the strict ordering is 8.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GREATER(s(x), s(y)) → GREATER(x, y)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

GREATER(s(x), s(y)) → GREATER(x, y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(GREATER(x₁, x₂)) = x_2
POL(s(x₁)) = 1 + x_1

The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y), s(z)) → LE(x, y, z)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

LE(s(x), s(y), s(z)) → LE(x, y, z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(s(x₁)) = 1/4 + x_1
POL(LE(x₁, x₂, x₃)) = (1/2)x_2

The value of delta used in the strict ordering is 1/8.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)

The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.